Merge pull request #1822 from antonio-nino-diaz-arm/an/plat-arm
authorAntonio Niño Díaz <[email protected]>
Fri, 15 Feb 2019 11:03:06 +0000 (11:03 +0000)
committerGitHub <[email protected]>
Fri, 15 Feb 2019 11:03:06 +0000 (11:03 +0000)
docs: Update note about plat/arm in Porting Guide


Trivial merge